Cálculos de múltipla conclusão para a lógica intuicionista sob uma perspectiva geométrica

Abstract

Como verificar se uma prova clássica também é intuicionista? Em dedução natural basta não haver ocorrência da lei do terceiro excluído ou da eliminação da dupla negação, conforme proposto por Gentzen. No seu cálculo de sequentes o mesmo resultado é alcançado restringindo o número de fórmulas no lado direito a no máximo um. Assim não há múltiplaconclusão, embora esta seja importante para a simetria. Hoje já existem abordagens que levam isso em conta e propõem cálculos de sequentes para lógica intuicionista com várias fórmulas no consequente. Mas ainda que elas nos forneçam compreensões do que diferencia a lógica intuicionista da clássica, há o problema da burocracia inerente ao formalismo de Gentzen. Aqui separamos a lógica intuicionista da clássica em derivações não-sequenciais adotando uma abordagem geométrica. Propomos uma versão intuicionista para dois sistemas de múltipla conclusão inicialmente definidos apenas para a lógica clássica proposicional: os N-Grafos, apresentados por de Oliveira (2001) e baseado em dedução natural; e as proof-nets de Robinson (2003), inspiradas no cálculo de sequentes.